SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
Identifieur interne : 003030 ( Main/Exploration ); précédent : 003029; suivant : 003031SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
Auteurs : Michael Codish [Israël] ; Jürgen Giesl [Allemagne] ; Peter Schneider-Kamp [Danemark] ; René Thiemann [Autriche]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2012-06-01.
English descriptors
Abstract
Abstract: This paper introduces a propositional encoding for recursive path orders (RPO), in connection with dependency pairs. Hence, we capture in a uniform setting all common instances of RPO, i.e., lexicographic path orders (LPO), multiset path orders (MPO), and lexicographic path orders with status (LPOS). This facilitates the application of SAT solvers for termination analysis of term rewrite systems (TRSs). We address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (A) the lexicographic comparison w.r.t. a permutation of the arguments; (B) the multiset extension of a base order; (C) the combined search for a path order together with an argument filter to orient a set of inequalities; and (D) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-called usable rules). We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.
Url:
DOI: 10.1007/s10817-010-9211-0
Affiliations:
- Allemagne, Autriche, Danemark, Israël
- District de Cologne, Rhénanie-du-Nord-Westphalie
- Aix-la-Chapelle
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001430
- to stream Istex, to step Curation: 001413
- to stream Istex, to step Checkpoint: 000792
- to stream Main, to step Merge: 003087
- to stream Main, to step Curation: 003030
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs</title><author><name sortKey="Codish, Michael" sort="Codish, Michael" uniqKey="Codish M" first="Michael" last="Codish">Michael Codish</name></author><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></author><author><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name></author><author><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:56D86663364CCCC6BA55000A05126BD58936FD56</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/s10817-010-9211-0</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-8LVLT91M-S/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001430</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001430</idno><idno type="wicri:Area/Istex/Curation">001413</idno><idno type="wicri:Area/Istex/Checkpoint">000792</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000792</idno><idno type="wicri:doubleKey">0168-7433:2010:Codish M:sat:solving:for</idno><idno type="wicri:Area/Main/Merge">003087</idno><idno type="wicri:Area/Main/Curation">003030</idno><idno type="wicri:Area/Main/Exploration">003030</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs</title><author><name sortKey="Codish, Michael" sort="Codish, Michael" uniqKey="Codish M" first="Michael" last="Codish">Michael Codish</name><affiliation wicri:level="1"><country xml:lang="fr">Israël</country><wicri:regionArea>Department of Computer Science, Ben-Gurion University of the Negev, PoB 653, 84105, Beer-Sheva</wicri:regionArea><wicri:noRegion>Beer-Sheva</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Israël</country></affiliation></author><author><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>LuFG Informatik 2, RWTH Aachen University, Ahornstr. 55, 52074, Aachen</wicri:regionArea><placeName><region type="land" nuts="1">Rhénanie-du-Nord-Westphalie</region><region type="district" nuts="2">District de Cologne</region><settlement type="city">Aix-la-Chapelle</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name><affiliation wicri:level="1"><country xml:lang="fr">Danemark</country><wicri:regionArea>Department of Mathematics & Computer Science, University of Southern Denmark, Campusvej 55, 5230, Odense M</wicri:regionArea><wicri:noRegion>Odense M</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Danemark</country></affiliation></author><author><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name><affiliation wicri:level="1"><country xml:lang="fr">Autriche</country><wicri:regionArea>Institute of Computer Science, University of Innsbruck, Techniker Str. 21a, 6020, Innsbruck</wicri:regionArea><wicri:noRegion>Innsbruck</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Autriche</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Springer Netherlands</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2012-06-01">2012-06-01</date><biblScope unit="volume">49</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="53">53</biblScope><biblScope unit="page" to="93">93</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Dependency pairs</term><term>Recursive path order</term><term>SAT solving</term><term>Term rewriting</term><term>Termination</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper introduces a propositional encoding for recursive path orders (RPO), in connection with dependency pairs. Hence, we capture in a uniform setting all common instances of RPO, i.e., lexicographic path orders (LPO), multiset path orders (MPO), and lexicographic path orders with status (LPOS). This facilitates the application of SAT solvers for termination analysis of term rewrite systems (TRSs). We address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (A) the lexicographic comparison w.r.t. a permutation of the arguments; (B) the multiset extension of a base order; (C) the combined search for a path order together with an argument filter to orient a set of inequalities; and (D) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-called usable rules). We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>Autriche</li><li>Danemark</li><li>Israël</li></country><region><li>District de Cologne</li><li>Rhénanie-du-Nord-Westphalie</li></region><settlement><li>Aix-la-Chapelle</li></settlement></list><tree><country name="Israël"><noRegion><name sortKey="Codish, Michael" sort="Codish, Michael" uniqKey="Codish M" first="Michael" last="Codish">Michael Codish</name></noRegion><name sortKey="Codish, Michael" sort="Codish, Michael" uniqKey="Codish M" first="Michael" last="Codish">Michael Codish</name></country><country name="Allemagne"><region name="Rhénanie-du-Nord-Westphalie"><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></region><name sortKey="Giesl, Jurgen" sort="Giesl, Jurgen" uniqKey="Giesl J" first="Jürgen" last="Giesl">Jürgen Giesl</name></country><country name="Danemark"><noRegion><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name></noRegion><name sortKey="Schneider Kamp, Peter" sort="Schneider Kamp, Peter" uniqKey="Schneider Kamp P" first="Peter" last="Schneider-Kamp">Peter Schneider-Kamp</name></country><country name="Autriche"><noRegion><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name></noRegion><name sortKey="Thiemann, Rene" sort="Thiemann, Rene" uniqKey="Thiemann R" first="René" last="Thiemann">René Thiemann</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003030 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 003030 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:56D86663364CCCC6BA55000A05126BD58936FD56
|texte= SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs
}}
| This area was generated with Dilib version V0.6.33. |  |